Nuprl Definition : mon
13,42
postcript
pdf
Mon == {
g
:GrpSig| IsMonoid(|
g
|;*;e) & IsEqFun(|
g
|;=
)}
latex
clarification:
Mon{i} == {
g
:GrpSig{i}| IsMonoid(|
g
|;*
g
;e
g
) & IsEqFun(|
g
|;=
g
)}
latex
Up
groups
1
Wellformedness Lemmas
mon
wf
Definitions
GrpSig
,
P
&
Q
,
IsMonoid(
T
;
op
;
id
)
,
*
,
e
,
IsEqFun(
T
;
eq
)
,
|
g
|
,
=
origin
)}
g)} )}
g)}